Welcome back!

It’s good to be here!

Let’s dust off and update some of our old toys for a new language called Pie.

Is it obvious that this is an Atom?

'atom

Not at all. What does Atom mean?

To be an Atom is to be an atom.^†

_______________

 ^†In Lisp, atoms are symbols, numbers, and many other things. Here, atoms are only symbols.

Then 'atom is an Atom because 'atom is an atom.

Is it obvious that this is an Atom?

'ratatouille

Yes, because 'ratatouille is also an atom.

But what does it precisely mean to be an atom?

Atoms are built from a tick mark directly followed by one or more letters and hyphens.^†

_______________

 ^†In Pie, only atoms use the tick mark.

So, is it obvious that

'is-it-obvious-that-this-is-an-atom

is an Atom?

Certainly, because atoms can contain hyphens.

What about

'–––

and

–––

and

'

Are they atoms?

'–––

is an atom because hyphens can appear anywhere in an atom;

–––

is not an atom because it’s missing the tick mark; and

'

is not an atom because it is neither followed by a letter nor by a hyphen.

Is 'Atom an Atom?

Yes, even 'Atom is an Atom, because it is a tick mark followed by one or more letters or hyphens.

Is 'at0m an Atom?

No, because atoms can contain only letters and hyphens, as mentioned in frame 5, and the character 0 is not a letter. It is the digit zero.

Is 'cœurs-d-artichauts an Atom?

Is 'ἂτομον an Atom?

That’s Greek to me!

But Greek letters are letters, so it must also be an Atom.

Sentences such as

'ratatouille is an Atom

and

'cœurs-d-artichauts is an Atom

are called judgments.^†

_______________

 ^†Thanks, Per Martin-Löf (1942–).

What is the point of a judgment?

A judgment is an attitude that a person takes towards expressions. When we come to know something, we are making a judgment.

What can be judged about Atom and 'courgette?

'courgette is an Atom.

A form of judgment is an observation with blank spaces in it, such as

____ is a ____.

Are there other forms of judgment?

Another form of “judgment” is “judgement.”

Very funny.

Is

'ratatouille

the same

Atom

as

'ratatouille?

Yes.

They are the same Atom because both have the same letters after the tick mark.

Is

'ratatouille

the same

Atom

as

'baguette?

No.

They have different letters after the tick mark.

The second form of judgment is that

____ is the same ____ as ____.

So

'citron is the same Atom as 'citron

is a judgment.

It is a judgment, and we have reason to believe it.

Is

'pomme is the same Atom as 'orange

a judgment?

It is a judgment, but we have no reason to believe it. After all, one should not compare apples and oranges.

Is it obvious that

(cons 'ratatouille 'baguette)^†

is a

(Pair Atom Atom)?

_______________

 ^†When ready, see page 62 for “typing” instructions.

No, it isn’t.

What does it mean to be a

(Pair Atom Atom)?

To be a

(Pair Atom Atom)

is to be a pair whose car is an Atom, like 'ratatouille, and whose cdr is also an Atom, like 'baguette.

The names cons, car, and cdr seem familiar. What do they mean again? And what do they have to do with pairs?

A pair begins with cons^† and ends with two more parts, called its car and its cdr.

_______________

 ^†In Lisp, cons is used to make lists longer. Here, cons only constructs pairs.

Okay. That means that

(cons 'ratatouille 'baguette)

is a

(Pair Atom Atom)

because (cons 'ratatouille 'baguette) is a pair whose car is an Atom, and whose cdr is also an Atom.

Is cons a Pair, then?

Neither cons nor Pair alone is even an expression. Both require two arguments.^†

Is

(cons 'ratatouille 'baguette)

the same

(Pair Atom Atom)

as

(cons 'ratatouille 'baguette)?

_______________

 ^†In Lisp, cons is a procedure and has meaning on its own, but forms such as cond or lambda are meaningless if they appear alone.

What does it mean for two expressions to be the same

(Pair Atom Atom)?

It means that both cars are the same Atom and that both cdrs are the same Atom.

Then

(cons 'ratatouille 'baguette)

is indeed the same

(Pair Atom Atom)

as

(cons 'ratatouille 'baguette).

Is

(cons 'ratatouille 'baguette)

the same

(Pair Atom Atom)

as

(cons 'baguette 'baguette)?

The car of

(cons 'ratatouille 'baguette)

is 'ratatouille, while the car of

(cons 'baguette 'baguette)

is 'baguette.

So we have no reason to believe that they are the same (Pair Atom Atom).

How can

(cdr

(cons 'ratatouille 'baguette))

be described?

It is an

Atom.

Expressions that describe other expressions, such as Atom, are called types.

Is (Pair Atom Atom)^† a type?

_______________

 ^†When a name, such as Pair or Atom, refers to a type, it starts with an upper-case letter.

Yes, because it describes pairs where the car and cdr are both Atoms.

The third form of judgment is

____is a type.

This means that both

Atom is a type

and

(Pair Atom Atom) is a type

are judgments.

Is

'courgette is a type

a judgment?

It is a judgment, but we have no reason to believe it because 'courgette doesn’t describe other expressions.

Are Atom and Atom the same type?

Presumably. They certainly look like they should be.

The fourth and final form of judgment is

____ and ____ are the same type.

Ah, so

Atom and Atom are the same type

is a judgment, and we have reason to believe it.

Is this a judgment?

Atom and (Pair Atom Atom) are the

same type.

Yes, it is a judgment, but there is no reason to believe it.

Are

(Pair Atom Atom)

and

(Pair Atom Atom)

the same type?

That certainly seems believable.

Judgments are acts of knowing, and believing is part of knowing.

Aren’t judgments sentences?

Sentences get their meaning from those who understand them. The sentences capture thoughts that we have, and thoughts are more important than the words we use to express them.

Ah, so coming to know that

(Pair Atom Atom)

and

(Pair Atom Atom)

are the same type was a judgment?

It was.

Is 'pêche the same 'fruit as 'pêche?

Good question.

Is 'pêche a 'fruit?

No, it is not, because

'fruit is a type

is not believable.

Some forms of judgment only make sense after an earlier judgment.^†

_______________

 ^†This earlier judgment is sometimes called a presupposition.

Which are these?

To ask whether an expression is described by a type, one must have already judged that the supposed type is a type. To ask whether two expressions are the same according to a type, one must first judge that both expressions are described by the type.^†

What judgment is necessary before asking whether two expressions are the same type?

_______________

 ^†To describe the expressions, the supposed type must also be a type.

To ask whether two expressions are the same type, one must first judge that each expression is, in fact, a type.

Is

(car

(cons 'ratatouille 'baguette))

the same

Atom

as

'ratatouille?

This looks familiar. Presumably, car finds the car of a pair, so they are the same.

Is

(cdr

(cons 'ratatouille 'baguette))

the same

Atom

as

'baguette?

It must certainly be, because the cdr of the pair is 'baguette.

So

(car

(cons

(cons 'aubergine 'courgette)

'tomato))

is a …

… (Pair Atom Atom),

because

(cons 'aubergine 'courgette)

is a pair whose car is the Atom 'aubergine and whose cdr is the Atom 'courgette.

Is

(car

(cdr

(cons 'ratatouille

(cons 'baguette 'olive-oil))))

the same

Atom

as

'baguette?

Yes, it is.

Expressions that are written differently may nevertheless be the same, as seen in frames 39–41. One way of writing these expressions is more direct than the others.

'baguette certainly seems more direct than

(car

(cdr

(cons 'ratatouille

(cons 'baguette 'olive-oil)))).

The normal form of an expression is the most direct way of writing it. Any two expressions that are the same have identical normal forms, and any two expressions with identical normal forms are the same.

Is 'olive-oil the normal form of

(cdr

(cdr

(cons 'ratatouille

(cons 'baguette 'olive-oil))))?

That question is incomplete.

Sameness is always according to a type, so normal forms are also determined by a type.

Is 'olive-oil the normal form of the Atom

(cdr

(cdr

(cons 'ratatouille

(cons 'baguette 'olive-oil))))?

Yes, it is.

Is

(cons 'ratatouille 'baguette)

a normal

(Pair Atom Atom)?^†

_______________

 ^†Normal is short for in normal form.

Yes, (cons 'ratatouille 'baguette) is normal.

Does every expression have a normal form?

It does not make sense to ask whether an expression has a normal form without specifying its type.

Given a type, however, every expression described by that type does indeed have a normal form determined by that type.

If two expressions are the same according to their type, then they have identical normal forms. So this must mean that we can check whether two expressions are the same by comparing their normal forms!

What is the normal form of

(car

(cons

(cons 'aubergine 'courgette)

'tomato))?

What about the type?

If the type is

(Pair Atom Atom),

then the normal form is

(cons 'aubergine 'courgette).

Nice catch!

The previous description of what it means to be a

(Pair Atom Atom)

is incomplete. It must mean …

… to be a pair whose car is an Atom, and whose cdr is also an Atom, or an expression that is the same as such a pair.

Is

(car

(cons

(cons 'aubergine 'courgette)

'tomato))

the same

(Pair Atom Atom)

as

(cons 'aubergine 'courgette)?

Yes, the two expressions are the same (Pair Atom Atom) because the normal form of

(car

(cons

(cons 'aubergine 'courgette)

'tomato))

is

(cons 'aubergine 'courgette).

Why is

(cons 'aubergine 'courgette)

the same (Pair Atom Atom) as

(cons 'aubergine 'courgette)?

That seems pretty obvious.

Yes, but not everything that seems obvious is actually obvious.^†

Frame 23 describes what it means for one expression to be the same

(Pair Atom Atom)

as another.

_______________

 ^†In Lisp, two uses of cons with the same atoms yield pairs that are not eq. Here, however, they cannot be distinguished in any way.

Both

(cons 'aubergine 'courgette)

and

(cons 'aubergine 'courgette)

have cons at the top. 'aubergine is the same Atom as 'aubergine, and 'courgette is the same Atom as 'courgette.

Both expressions have the same car and have the same cdr. Thus, they are the same

(Pair Atom Atom).

Perfect.

What is the normal form of

(Pair

(cdr

(cons Atom 'olive))

(car

(cons 'oil Atom)))?

It is (Pair 'olive 'oil), right?

Actually, the expression

(Pair

(cdr

(cons Atom 'olive))

(car

(cons 'oil Atom)))

is neither described by a type, nor is it a type, so asking for its normal form is meaningless.^†

_______________

 ^†Expressions that cannot be described by a type and that are not themselves types are also called ill-typed.

Why not?

Because Pair is not a type when its arguments are actual atoms.

It is only an expression when its arguments are types such as Atom.

Does that mean that Pair can’t be used together with car and cdr?

No, not at all. What is the normal form of

(Pair

(car

(cons Atom 'olive))

(cdr

(cons 'oil Atom)))?

What is its type? Normal forms are according to a type.

Types themselves also have normal forms. If two types have identical normal forms, then they are the same type, and if two types are the same type, then they have identical normal forms.

The normal form of the type

(Pair

(car

(cons Atom 'olive))

(cdr

(cons 'oil Atom)))?

must be (Pair Atom Atom) because the normal form of

(car

(cons Atom 'olive))

is Atom and the normal form of

(cdr

(cons 'oil Atom))

is Atom.

That’s it. Now we know that

(cons 'ratatouille 'baguette)

is also a

(Pair

(car

(cons Atom 'olive))

(cdr

(cons 'oil Atom)))

because …

… the normal form of

(Pair

(car

(cons Atom 'olive))

(cdr

(cons 'oil Atom)))

is

(Pair Atom Atom),

and

(cons 'ratatouille 'baguette)

is a

(Pair Atom Atom).

Another way to say this is that

(Pair

(car

(cons Atom 'olive))

(cdr

(cons 'oil Atom)))

and

(Pair Atom Atom)

are the same type.

If an expression is a

(Pair

(car

(cons Atom 'olive))

(cdr

(cons 'oil Atom)))

then it is also a

(Pair Atom Atom)

because those two types are the same type.

Similarly, if an expression is a

(Pair Atom Atom)

then it is also a

(Pair

(car

(cons Atom 'olive))

(cdr

(cons 'oil Atom)))

because those two types are the same type.

And likewise for

(Pair

Atom

(cdr

(cons 'oil Atom))),

which is also the same type.

Is '6 an Atom?

No. We have no reason to believe that

'6 is an Atom,

because the digit 6 is neither a letter nor a hyphen, right?

Right. Is

(cons '17 'pepper)

a

(Pair Atom Atom)?

No, because the car of (cons '17 'pepper) is '17, which is not an Atom.

It sure would be natural to have numbers, though.

Numbers are certainly convenient. Besides Atom and Pair, we can check whether something is a Nat.

Let’s give it a try.

Is 1 a Nat?^†

_______________

 ^†Nat is a short way of writing natural number.

Yes, 1 is a Nat.

Is 1729 a Nat?

Yes, 1729 is a Nat. Not only is it a Nat, it’s also famous!^†

_______________

 ^†Thank you, Srinivasa Ramanujan (1887–1920) and Godfrey Harold Hardy (1877–1947).

Is −1 a Nat?

Hmm. Sure?

No, it isn’t. What about −23?

It’s not very clear.

Positive numbers are Nats.

Ah, then −23 is not a Nat?

We prefer a positive point of view.

What is the smallest Nat?

Isn’t 0 a natural number?

Oh yeah, one can’t always be positive.^† How can one get the rest of the Nats?

_______________

 ^†The number 1, however, is always positive.

One can use our old friend add1. If n is a Nat, then (add1 n) is also a Nat, and it is always a positive Nat even if n is 0.

How many Nats are there?

Lots!

Is there a largest Nat?

No, because one can always …

… add one with add1?

That’s right!^†

Is 0 the same Nat as 26?

_______________

 ^†Thank you, Giuseppe Peano (1838–1932).

Clearly not.

Is (+ 0 26)^† the same as 26?

_______________

 ^†Even though we have not explained + yet, use your knowledge of addition for now.

Of course.

Is (+ 0 26) the same Nat as 26?

Yes, because the normal form of (+ 0 26) is 26, and 26 is certainly the same as 26.

What does zero mean?

Does zero mean the same as 0?

In Pie, zero and 0 are two ways to write the same Nat.

Is one the same Nat as 1?

Well, if zero is the same Nat as 0, that would make sense.

Actually, one has no meaning. But (add1 zero) is another way to write the number 1.

It is possible to make one be (add1 zero) by defining it.

Why is the box around the definition dashed?

A dashed box means that there is something the matter with the definition, so the definition in the dashed box is not available for use later.

What is the matter with that definition?

It looks okay.

When defining a name, it is necessary to first claim the name with a type, and one is a Nat.

So two can be defined as

If 1 is another way of writing (add1 zero), what is another way of writing 4?

Shouldn’t it be

(add1

(add1

(add1

(add1 zero))))?

Can’t we define four to mean that?

Of course.

Is there another way of writing 8 as well?

It must be

(add1

(add1

(add1

(add1

(add1

(add1

(add1

(add1 zero)))))))).

Is 8 normal?

It seems that way. But why is 8 normal?

8 is normal because its top^† add1 is a constructor, and because the argument tucked under the top add1, namely 7, is normal.

_______________

 ^†The top add1 in frame 81 is underlined this one time for emphasis.

Why is 7, also written

(add1

(add1

(add1

(add1

(add1

(add1

(add1 zero))))))),

normal?

7 is normal for the very same reason.

This must mean that zero is normal, or else (add1 zero) would not be normal.

What is at the top of zero?

It must be zero.

zero is normal because the top zero is a constructor, and it has no arguments.

Is

(add1

(+ (add1 zero)

(add1

(add1 zero))))

normal?

No, because + is not a constructor.

An expression with a constructor at the top is called a value.^†

Even though

(add1

(+ (add1 zero)

(add1

(add1 zero))))

is not normal, it is a value.

_______________

 ^†Values are also called canonical expressions.

It is not normal because

(+ (add1 zero)

(add1

(add1 zero)))

is not the most direct way of writing 3.

Here’s another expression that is not normal.

(+ (add1

(add1 zero))

(add1 zero))

Is this the most direct way of writing 3?

No.

What exactly is a constructor?

Some expressions, such as Nat or (Pair Nat Atom), are types.

Part of explaining a new type is to say what its constructors are. The constructor expressions are the direct ways of building expressions with the new type.

What are some examples of constructors?

The constructors of Nat are zero and add1, while the constructor of Pair is cons.

What is the relationship between values and normal forms?

In a value, the top constructor’s arguments need not be normal, but if they are, then the entire constructor expression is in normal form.

Are all values normal?

No.

(add1

(+ (add1 zero)

(add1

(add1 zero))))

and

(add1

(+ (add1 zero) (add1 one)))

are values, but they are not normal.

What expressions can be placed in the empty box to make this expression not a Nat value?

(add1

)

How about 'aubergine?

Indeed,

(add1

'aubergine)

is not a Nat value because 'aubergine is an Atom, not a Nat.

When filling in boxes, the expectation is that the resulting expression is described by a type.

If any Nat expression is placed in the box, however, the whole expression is a value. The whole expression has add1 at the top, and add1 is a Nat constructor.

Finding a value that is the same as some starting expression is called evaluation.

What about the type? Sameness, after all, requires types.

From time to time, when talking about sameness, we do not explicitly mention a type. Nevertheless, a type is always intended, and can be discovered by reading carefully.

Doesn’t evaluation refer to finding the meaning of an expression, not just some simpler expression?

Not here. Expressions do not refer to some external notion of meaning—in Pie, there is nothing but expressions and what we judge about them.^†

_______________

 ^†In Lisp, values are distinct from expressions, and the result of evaluation is a value.

That is a new way of seeing evaluation.

Why is there a difference between normal forms and values?

A normal expression has no remaining opportunities for evaluation. Usually, expressions that are normal are easier to understand. Finding a value is often enough, however, because the top constructor can be used to determine what must happen next.

If finding a value is often enough, does that mean we are free to find the value and stop whenever we want?

Yes, assuming that specific information about the constructor’s arguments is never needed.

Is

(add1

(+ (add1 zero)

(add1

(add1 zero))))

the same Nat as four?

Here is a possible answer.

They are not the same Nat because

(add1

(+ (add1 zero)

(add1

(add1 zero))))

is a value, and it certainly does not look like the variable four. Finding the value of four does not help, because four’s value looks very different.

Good try.

But they are actually the same Nat.

How can that be?

Two Nat expressions, that aren’t values, are the same if their values are the same. There are exactly two ways in which two Nat values can be the same: one for each constructor.

If both are zero, then they are the same Nat.

What about when both values have add1 at the top?

If the arguments to each add1 are the same Nat, then both add1-expressions are the same Nat value.

Why is

(add1 zero)

the same

Nat

as

(add1 zero)?

Both expressions are values. Both values have add1 at the top, so their arguments should be the same Nat.

The arguments are both zero, which is a value, and zero is the same Nat value as zero.

Why is

(add1 (+ 0 1))

the same

Nat

as

(add1 (+ 1 0))?

Both of these Nats have add1 at the top, so they are values.

They are the same because

(+ 0 1)

is the same

Nat

as

(+ 1 0).

Why is (+ 0 1) the same Nat as (+ 1 0)?

These Nats are not values, so to determine whether they are the same, the first step is to find their values.

Both expressions have (add1 zero) as a value, and frame 101 explains why

(add1 zero)

is the same

Nat

as

(add1 zero).

That’s right.

Does this mean that four could have been defined like this?

Why is that box dashed?

four is already defined, and can’t be defined again.

And yes, four could have been defined like that initially.

In fact, no other expression could tell the difference between the two definitions of four because both define four to be the same Nat.

Is cons a constructor?

Yes, cons constructs Pairs.

Is it necessary to evaluate car’s argument in order to evaluate a car-expression?

Yes. To find the value of a car-expression, start by finding the value of its argument.

What can be said about the argument’s value?

The argument’s value has cons at the top.

After finding the argument’s value, what comes next?

The value is the first argument to cons.

What is the value of

(car

(cons (+ 3 5) 'baguette))?

The first argument to cons is

(+ 3 5),

which is not a value.

To find the value of a car-expression, first find the value of the argument, which is (cons a d).^† The value of

(car

(cons a d))

is then the value of a.

How can the value of a cdr-expression be found?

_______________

 ^†Here, a is for car and d is for cdr.

Like car, start by evaluating cdr’s argument until it becomes (cons a d). Then, the value of

(cdr

(cons a d))

is the value of d.

Do all constructors have arguments?

No. Recall from frame 86 that zero is a constructor.

What does it mean for two expressions to be the same (Pair Atom Nat)?

It must mean that the value of each expression has cons at the top. And, their cars are the same Atom and their cdrs are the same Nat.

Very good.

Are atoms constructors?

The atom 'bay is a constructor, and so is the atom 'leaf.

Are all atoms constructors?

Yes. Each atom constructs itself.

Does this mean that atoms are values?

Yes, it does, because the explanation of why

Atom is a type

says that atoms are Atom values.

Right.

In the expression zero, what is the top constructor?

It must be zero, because zero is a constructor of no arguments.

In the expression 'garlic, what is the top constructor?

The atom 'garlic is the only constructor, so it must be the top constructor.

Is Nat a constructor, then?

No, Nat is not a constructor. zero and add1 are constructors that create data, while Nat describes data that is just zero, or data that has add1 at its top and another Nat as its argument.

Is Pair a constructor?

No, because Pair-expressions describe expressions with cons at the top. Constructors create data, not types.

What is Pair called, then?

Pair is a type constructor because it constructs a type. Likewise, Nat and Atom are type constructors.

Is

(cons zero 'onion)

a

(Pair Atom Atom)?

No.

Isn’t it a

(Pair Nat Atom)?

Indeed it is! But

(cons 'zero 'onion)

is a

(Pair Atom Atom).

What is the type of

(cons 'basil

(cons 'thyme 'oregano))?^†

_______________

 ^†Thank you, Julia Child (1912–2004).

Based on what we’ve seen, it must be a

(Pair Atom

(Pair Atom Atom)).

Indeed it is.

All right, that’s enough for now. My head is going to explode!

It might be a good idea to read this chapter one more time. Judgments, expressions, and types are the most important ideas in this book.

Some fresh vegetables would be nice after all this reading.

How was the ratatouille?

Très bien, thanks for asking.

In chapter 1, there are constructors, which build values, and type constructors, which build types.

car, however, is neither a constructor nor a type constructor.

What is car, then?

car is an eliminator. Eliminators take apart the values built by constructors.

What is another eliminator?

If car is an eliminator, then surely cdr is also an eliminator.

Another way to see the difference is that values contain information, and eliminators allow that information to be used.

Is there anything that is both a constructor and an eliminator?

No, there is not.

It is possible to define a function that is as expressive as both car and cdr combined.

How?

It requires our old friend λ.

What is that? It doesn’t look familiar.

Oops! It is also known as lambda.^†

_______________

 ^†λ can be optionally written lambda.

Oh, right, λ builds functions.

Does this mean that λ is a constructor?

Yes, it does, because every expression that looks like (λ (x₀ x … ^†) body) is a value.

What is the eliminator for such values?

_______________

 ^†The notation x … means zero or more xs, so x₀ x … means one or more xs.

The only thing that can be done to a function is to apply it to arguments.

How can functions have an eliminator?

Applying a function to arguments is the function’s eliminator.

Okay.

What is the value of

(λ (flavor)

(cons flavor 'lentils))?

It starts with a λ, so it is already a value.

Right.

What is the value of

((λ (flavor)

(cons flavor 'lentils))

'garlic)?

It must be (cons 'garlic 'lentils), if λ works the same way as lambda and cons is a constructor.

But doesn’t this mean that cons’s first argument is being evaluated, even though the cons-expression is already a value?

No, it does not, but that’s a very good question. Replacing the λ-expression’s flavor happens because the λ-expression is applied to an argument, not because of the cons.^†

Every flavor in the body of the λ-expression is replaced with 'garlic, no matter what expression surrounds the flavor.

_______________

 ^†Consistently replacing a variable with an expression is sometimes called substitution.

So this means that the value of

((λ (root)

(cons root

(cons (+ 1 2) root)))

'potato)

is therefore

(cons 'potato

(cons (+ 1 2) 'potato)),

right?

Why is there is no need to evaluate

(+ 1 2)

in the preceding frame?

The entire expression has cons at the top, so it is a value.

Frame 12 contains a small exaggeration. If the root (underlined here) in the body of the λ-expression occurs under another λ with the same name, then it is not replaced.

What is the value of

((λ (root)

(cons root

(λ (root)

root)))

'carrot)?

It must be

(cons 'carrot

(λ (root)

root))

because the inner root is under a λ-expression with the same name.

λ does work the same way as lambda, and that is indeed the right answer.

To be an

(→ Atom

(Pair Atom Atom))^†

is to be a λ-expression that, applied to an Atom as its argument, evaluates to a

(Pair Atom Atom).

_______________

 ^†This is pronounced “Arrow atom pause pair atom atom.” And → can be written with two characters: ->.

What about expressions that have these λ-expressions as their values?

Yes, these are also

(→ Atom

(Pair Atom Atom))

because they too become a

(Pair Atom Atom)

when given an Atom as an argument.

Are they also

(→ (car (cons Atom 'pepper))

(Pair (cdr (cons 'salt Atom)) Atom))?

Yes, because

(car

(cons Atom 'pepper))

is Atom and

(cdr

(cons 'salt Atom))

is also Atom.

It makes sense to ask what it means for two expressions to be the same Nat, the same Atom, or the same (Pair Nat Atom).

Does it also make sense to ask what it means for two expressions to be the same

(→ Nat

Atom),

or the same

(→ (Pair Atom Nat)

Nat)?

Yes, it does. Two expressions are the same

(→ Nat

Atom)

when their values are the same

(→ Nat

Atom).

Their values are λ-expressions. What does it mean for two λ-expressions to be the same

(→ Nat

Atom)?

Two λ-expressions that expect the same number of arguments are the same if their bodies are the same. For example, two λ-expressions are the same

(→ Nat

(Pair Nat Nat))

if their bodies are the same

(Pair Nat Nat).

Does this mean that

(λ (x)

(cons x x))

is not the same

(→ Nat

(Pair Nat Nat))

as

(λ (y)

(cons y y))?

What is not the same about those expressions?

The names of the arguments are different. This usually doesn’t matter, though. Does it matter here?

Two λ-expressions are also the same if there is a way to consistently rename the arguments to be the same that makes their bodies the same.^†

Consistently renaming variables can’t change the meaning of anything.

_______________

 ^†Renaming variables in a consistent way is often called alpha-conversion. Thank you, Alonzo Church (1903–1995).

Is

(λ (a d)

(cons a d))

the same

(→ Atom Atom

(Pair Atom Atom))

as

(λ (d a)

(cons a d))?

No, it is not, because consistently renaming the variables in the second λ-expression to match the arguments in the first λ-expression yields

(λ (a d)

(cons d a)),

and (cons d a) is not the same (Pair Atom Atom) as (cons a d).

What about

(λ (y)

(car

(cons y y)))?

Is it the same

(→ Nat

Nat)

as

(λ (x)

x)?

First, consistently rename y to x. Now, the question is whether

(car

(cons x x))

is the same Nat as x.

There are precisely two ways that two expressions can be the same Nat. One way is for both their values to be zero. The other is for both their values to have add1 at the top and for the arguments to both add1s to be the same Nat.

These expressions are not Nat values because they do not have add1 at the top and they are not zero.

… because the λ-expression is an

(→ Nat

Nat),

so the argument x can’t be anything else.

Expressions that are not values and cannot yet be evaluated due to a variable are called neutral.

Does this mean that

(cons y 'rutabaga)

is neutral?

No, it is not neutral, because

(cons y 'rutabaga)

is a value.

If x is a (Pair Nat Atom), is

(cdr x)

a value?

No, because cdr is an eliminator, and eliminators take apart values.

Without knowing the value of x, there is no way to find the value of (cdr x), so (cdr x) is neutral.

Neutral expressions make it necessary to expand our view on what it means to be the same. Each variable is the same as itself, no matter what type it has. This is because variables are only replaced consistently, so two occurrences of a variable cannot be replaced by values that are not the same.

So if we assume that y is a Nat, then

(car

(cons y 'rutabaga))

is the same Nat as y because the car-expression’s normal form is y, and y is the same Nat as y.

Yes. And, likewise,

(λ (x)

(car

(cons x x)))

is the same

(→ Nat

Nat)

as

(λ (x)

x).

Right, because the neutral expression x is the same Nat as x.

Is

(λ (x)

(car x))

the same

(→ (Pair Nat Nat)

Nat)

as

(λ (y)

(car y))?

One would think so. But why?

The first step is to consistently rename y to x.

Is

(λ (x)

(car x))

the same

(→ (Pair Nat Nat)

Nat)

as

(λ (x)

(car x))?

Yes, assuming that

(car x)

is the same Nat as

(car x).

But (car x) is not a variable, and it is not possible to find its value until x’s value is known.

If two expressions have identical eliminators at the top and all arguments to the eliminators are the same, then the expressions are the same. Neutral expressions that are written identically are the same, no matter their type.

So

(car x)

is indeed the same Nat as

(car x),

assuming that x is a (Pair Nat Nat).

Is

(λ (a d)

(cons a d))

an

(→ Atom Atom

(Pair Atom Atom))?

What does having more expressions after the → mean?

The expressions after an →, except the last^† one, are the types of the arguments. The last one is the value’s type.

_______________

 ^†The last one is preceded by a pause when pronounced.

Okay, then,

(λ (a d)

(cons a d))

is an

(→ Atom Atom

(Pair Atom Atom)).

These expressions are certainly getting long.

One way to shorten them is the careful use of define, as in frame 1:77, which allows short names for long expressions.

Good idea.

Suppose that the constructor cons is applied to 'celery and 'carrot. We can refer to that value as vegetables.

From now on, whenever the name vegetables is used, it is the same

(Pair Atom Atom)

as

(cons 'celery 'carrot),

because that is how vegetables is defined.

Why does it say

(Pair Atom Atom)

after claim?

(Pair Atom Atom) describes how we can use vegetables—we know that

(car vegetables) is an Atom, and also that (cons 'onion vegetables) is a

(Pair Atom

(Pair Atom Atom)).^†

_______________

 ^†They are a good start for lentil soup, too.

Ah, that makes sense.

Is

vegetables

the same

(Pair Atom Atom)

as

(cons (car vegetables)

(cdr vegetables))?

Yes, because the value of each expression is a pair whose car is 'celery and whose cdr is 'carrot.

In fact, whenever

p is a (Pair Atom Atom),

then

p is the same

(Pair Atom Atom)

as

(cons (car p) (cdr p)).

Finding the values of (car p) and (cdr p) is not necessary.

That seems reasonable.

Is this definition allowed?

What?

It is allowed, even though it is probably a foolish idea.

What would be the normal form of

(+ five 5)?

It must be 10 because five plus 5 is ten.

Try again. Remember the strange definition of five …

… Oh, right, it would be 14 if five were defined to be 9.

That’s right

Is this definition allowed? It doesn’t seem particularly foolish.

It is not as foolish as defining five to mean 9, but it is also not allowed.

Names that are already used, whether for constructors, eliminators, or previous definitions, are not suitable for use with claim or define.

Okay.

There is an eliminator for Nat that can distinguish between Nats whose values are zero and Nats whose values have add1 at the top. This eliminator is called which-Nat.

How does which-Nat tell which of the two kinds of Nats it has?

A which-Nat-expression has three arguments: target, base, and step:

(which-Nat target

base

step).

which-Nat checks whether

target is zero.

If so,

the value of the which-Nat-expression

is

the value of base.

Otherwise, if

target is (add1 n),

then

the value of the which-Nat-expression

is

the value of (step n).

So which-Nat both checks whether a number is zero and removes the add1 from the top when the number is not zero.

Indeed.

What is the normal form of

(which-Nat zero

'naught

(λ (n)

'more))?

It must be 'naught because the target, zero, is zero, so the value of the which-Nat-expression is base, which is 'naught.

Why is n written dimly?

The dimness indicates that n is not used in the body of the λ-expression. Unused names are written dimly.

Why isn’t it used?

which-Nat offers the possibility of using the smaller Nat, but it does not demand that it be used. But to offer this possibility, which-Nat’s last argument must accept a Nat.

Okay.

What is the value of

(which-Nat 4

'naught

(λ (n)

'more))?

It must be 'more because 4 is another way of writing (add1 3), which has add1 at the top. The normal form of

((λ (n)

'more)

3)

is

'more.

What is the normal form of

(which-Nat 5

0

(λ (n)

(+ 6 n)))?

Is it 11 because

((λ (n)

(+ 6 n))

5)

is 11?

The normal form is 10 because the value of a which-Nat expression is determined by the Nat tucked under the target as an argument to the step.

Ah, so the normal form is 10 because

((λ (n)

(+ 6 n))

4)

is 10.

Define a function called gauss^† such that (gauss n) is the sum of the Nats from zero to n.

What is the type of gauss?

_______________

 ^†Carl Friedrich Gauss (1777–1855), according to folklore, figured out that when he was in primary school and was asked to sum a long series.

The sum of Nats is a Nat.

Right.

Now define it.

How?

The first step is to choose an example argument. Good choices are somewhere between 5 and 10—they’re big enough to be interesting, but small enough to be manageable.

How about 5, then?

Sounds good.

What should the normal form of

(gauss 5)

be?

It should be 0 + 1 + 2 + 3 + 4 + 5, which is 15.

The next step is to shrink the argument.

(gauss 4), which is 10, is almost

(gauss 5), which is 15.

A white box around a gray box contains unknown code that wraps a known expression. What should be in this white box to get

(gauss 5)

from

(gauss 4)?

5 must be added to (gauss 4), and our sum is 15.

Next, make it work for any Nat that has add1 at the top.

If n is a Nat, then what should be in the box to get

(gauss (add1 n))

from

(gauss n)?

Remember that 5 is another way of writing (add1 4).

The way to find (gauss (add1 n)) is to replace 4 with n in the preceding frame’s answer.

What about zero?

What is (gauss zero)?

Clearly it is 0.

Now define gauss.

Remember the white and gray boxes.

Piece of cake! The name, n-1, suggests that it represents a Nat that is tucked under (or one less than) n.

Nice try, and it would deserve a solid box if recursion were an option, but recursion is not an option.

Why not?

Because recursion is not an option.

Why not?

Because recursion is not an option.

Okay. Please explain why recursion is not an option.

Recursion is not an option because every expression must have a value. Some recursive definitions make it possible to write expressions that do not have values.

What is an example of a recursive definition and an expression without a value?

forever is such a definition.

What is the value of (forever 71)?

Good question.

Why does it have a dashed box?

Recursion is not an option, so recursive definitions (like forever) stay dashed forever.

But what about definitions like gauss that need recursion?

There is a safe alternative to recursive definitions. This alternative allows gauss, along with many similar definitions, to be written without including the name gauss.

Here is the start of a safe alternative definition of gauss.

As far as it goes, it is correct. The point is that gauss cannot occur in its own definition.

Now it is clear what is meant by “Recursion is not an option.”

Does this mean that it is impossible to write gauss in Pie?

It is possible to write gauss in Pie, but which-Nat and define are not up to the task. A different eliminator is needed, but the time is not yet ripe.

Patience is a virtue.

It is also possible to define shorter names for expressions such as (Pair Nat Nat).

What is the claim in this case?

Another good question!

Expressions such as Atom, Nat, and (Pair Atom Nat), are types, and each of these types is a U.^†

_______________

 ^†U, pronounced “you,” is short for universe, because it describes all the types (except for itself).

Are types values?

Some types are values.

An expression that is a type is a value when it has a type constructor at its top. So far, we have seen the type constructors Nat, Atom, Pair, →, and U.

Are all types values?

No.

(car

(cons Atom 'prune))

is a type, but not a value, because car is neither a constructor nor a type constructor.

Which expressions are described by

(car

(cons Atom 'prune))?

Because

(car

(cons Atom 'prune))

and

Atom

are the same type,

(car

(cons Atom 'prune))

describes the same expressions as Atom.

What is the difference between type constructors and constructors?

Type constructors construct types, and constructors (or data constructors) construct values that are described by those types.

Judging that an expression is a type requires knowing its constructors. But the meaning of U is not given by knowing all the type constructors, because new types can be introduced.

Is (cons Atom Atom) a U?

No, but

(cons Atom Atom)

is a

(Pair U U).

An atom, like 'plum, is an Atom. On the other hand, Atom is not an Atom, it’s a type described by U.

Let’s think about (Pair Atom Atom).

Is

(cons Atom Atom)

a

(Pair Atom Atom)?

No, it is not, because Atom is a type, not an Atom.

Is U a U?

No, but U is a type. No expression can be its own type.^†

_______________

 ^†It would be possible for U to be a U₁, and U₁ to be a U₂, and so forth. Thank you, Bertrand Russell (1872–1970), and thanks, Jean-Yves Girard (1947–). Here, a single U is enough because U is not described by a type.

Is every expression that is a U also a type?

Yes, if X is a U, then X is a type.

Is every type described by U?

Every expression described by U is a type, but not every expression that is a type is described by U.

Is

(cons Atom Nat)

a

(Pair U U)?

Yes, it is.

Define Pear to mean the type of pairs of Nats.

That must be

From now on, the meaning of Pear is

(Pair Nat Nat).

The name has only four characters, but the type has fourteen.

Is Pear the same type as (Pair Nat Nat), everywhere that it occurs?

Yes, by the Commandment of define.

Is (cons 3 5) a Pear?

Yes, because

(cons 3 5)

is a

(Pair Nat Nat),

and

Pear

is defined to be precisely that type.

That’s a good point.

Is Pear a value?

No. Names defined with define are neither type constructors nor constructors. Thus, they are not values.

Is there an eliminator for Pear?

Does that mean an eliminator that takes apart values of type Pear?

Yes.

An eliminator for Pear must allow the information in values with type Pear to be used.

What does it mean to allow the information to be used?

An eliminator for Pear that allows the information in any Pear to be used is one that applies a function to the two Nat arguments in the Pear.

Okay.

Which functions can be applied to two Nats as arguments?

What about an expression that exchanges the Nats?

How about

(λ (a d)

(cons d a))?

Very good. What about an expression that extracts the first Nat from a Pear?

That must be

(λ (a d)

a).

Very close. Actually, it would be

(λ (a d)

a).

Okay. But the expression is correct except for dimness, right?

Indeed. To get a value of type X^† from a Pear, one must have an expression of type

(→ Nat Nat

X).

What type does + have?

_______________

 ^†X can be any type at all.

It takes two Nats and produces a Nat, so it must be

(→ Nat Nat

Nat).

That’s right.

What would be the type of

(λ (a d)

(cons d a)),

when both a and d are Nats?

Clearly it must be

(→ Nat Nat

Pear),

which is the same as

(→ Nat Nat

(Pair Nat Nat)).

How can a

λ-expression

be used with a

Pear?

Try this:

Is there a way to write the claim of elim-Pear without using Pear or Pear-maker?

Yes, by replacing Pear-maker and both Pears with their respective definitions.

The names Pear and Pear-maker were never necessary. Is the name elim-Pear necessary?

When are definitions necessary?

Never!

That’s right. elim-Pear is the same as the λ-expression that is its definition.

What is the value of

(elim-Pear

(cons 3 17)

(λ (a d)

(cons d a)))?

How about

((λ (pear maker)

(maker (car pear) (cdr pear)))

(cons 3 17)

(λ (a d)

(cons d a)))?

That’s a good start. But it is not yet a value.

The value is (cons 17 3).

Because elim-Pear means the same thing as the λ-expression in its definition,

(car

(cons 3 17))

is the same Nat as 3,

(cdr

(cons 3 17))

is the same Nat as 17, and

((λ (a d)

(cons d a))

3 17)

is the same Pear as

(cons 17 3).

What does it mean to add two pears?

Is it just adding the first and second Nats of each pear?

Good guess.

What type does this pearwise addition have?

The type is

(→ Pear Pear

Pear),

right?

How can pearwise addition be defined using elim-Pear?

That’s pretty hard.

Won’t it be necessary to eliminate both pears because both of their Nats are part of the result?

Indeed.

Define pearwise+, so that

(pearwise+

(cons 3 8)

(cons 7 6))

is the same Pear as

(cons 10 14).

First, split anjou and bosc into their respective parts, then add their first parts and their second parts.

It might be a good idea to take a break, then come back and re-read this chapter.

Yes, that does seem like a good idea.

But how can we ever get to chapter 3?

By getting to chapter 3.

It’s a good thing recursion is not an option.

It’s time to play with Pie.

Isn’t it impolite to play with your food?

While pie is indeed a delicious food, Pie is a language, and a little playing around with it won’t hurt.

Let’s get started.

Using Pie is very much like a conversation: it accepts claims, definitions, and expressions and it replies with feedback.

What sort of feedback?

For claims and definitions, the feedback is whether they are meaningful. For expressions, the feedback is also the expression’s type and normal form.

What if they are not meaningful?

Pie explains what is wrong with them, and sometimes adds a helpful hint.

What might be wrong with an expression?

Eat your vegetables before the Pie.

Try typing

'spinach

and see what happens.

Pie responds with

(the Atom 'spinach).

What does the mean here?

It means that 'spinach is an Atom.

In Pie, an expression must either be a type or be described by a type. Pie can find the types of many expressions on its own, including atoms.

What about

(car 'spinach)?

That expression is not described by a type because 'spinach is not a pair.

Can Pie always determine the type that describes an expression?

No, sometimes Pie needs help.

In that case, use a the-expression^† to tell Pie which type is intended.

_______________

 ^†the-expressions are also referred to as type annotations.

For example?

Pie cannot determine the type of a cons-expression that stands alone.

Why not? Isn’t it obvious that

(cons 'spinach 'cauliflower)

is a

(Pair Atom Atom)?

It is obvious to us, but later, cons becomes more magnificent, and that increased power means that the type cannot be determined automatically.

How, then, can Pie determine that

(cons 'spinach 'cauliflower)

is a pair?

Try this:

(the (Pair Atom Atom)

(cons 'spinach 'cauliflower)).

So a the-expression associates an expression with its type, both in Pie’s feedback and in the expressions we write.

There are two kinds of expressions in Pie: those for which Pie can determine a type on its own, and those for which Pie needs our help.

Are there other ways to help Pie with types?

Yes. In chapter 1, claim is required before its associated define, which tells Pie what type to use for the definition’s meaning.

Why not just use claim and define every time Pie can’t determine the type of an expression?

That would work, but keeping all the names straight might be exhausting.

Are there any other ways to help Pie find a type?

There is one more way. If an expression is used somewhere where only one type makes sense, then that type is used.

What is an example of this?

While checking that

(the (Pair Atom

(Pair Atom Atom))

(cons 'spinach

(cons 'kale 'cauliflower)))

is described by a type, Pie uses

(Pair Atom Atom)

as a type for

(cons 'kale 'cauliflower).

Here, the inner cons doesn’t need a the because its type is coming from the outer cons’s type.

Are expressions with the at the top values?

No.

The value of

(the X e)

is the value of e.

So what is the value of

(car

(the (Pair Atom Nat)

(cons 'brussels-sprout 4)))?

The value is one little round 'brussels-sprout.

Now try this:

U

Pie said:

U

Why wasn’t it

(the U U)?

U is a type, but it does not have a type. This is because no expression can be its own type, as seen in the note in frame 2:77.

When an expression is a type, but does not have a type, Pie replies with just its normal form.

Are there any other types that don’t have the type U?

Yes. (Pair U U), (Pair Atom U), and

(→ U

U)

are all types that do not have U as their type.

Are there any other aspects of Pie that would be good to know?

This is enough for now. There’s time for more Pie later.

What’s the next step?

Have fun playing.

Sounds like a plan!

Here is the dashed definition of gauss from frame 2:59.

Now, it is time to define gauss properly, without explicit recursion.

Does that mean that we are about to define gauss like this?

Why are recursive definitions not an option?

Because they are not an option.

Exactly.

But some recursive definitions always yield a value.

Like gauss, right?

That’s right.

What is the normal form of (gauss 0)?

It is zero.

What is the value of (gauss 1)?

It is 1 because

_______________

^†When expressions are vertically aligned with a bar to their left, assume that “is the same as” follows all but the last one. This kind of chart is called a “same as” chart.

Is that the value?

Is there more to do?

Actually,

(add1 (gauss zero))

is already a value. Why?

Oh, because it has the constructor add1 at the top.

Exactly.

What is the normal form of (gauss 1)?

It is (add1 zero).

Why does (gauss 2) have a normal form?

Because (gauss 2)’s normal form relies only on the normal form of (gauss 1), which has a normal form, and the normal form of +.

Does + have a normal form?

All right.

Why does (gauss 3) have a normal form?

Because (gauss 3)’s normal form relies only on the normal form of (gauss 2), which has a normal form, and the normal form of +. For now, we’re assuming + has a normal form.

Why does (gauss (add1 k)) have a normal form for any Nat k?

Because

(gauss (add1 k))’s normal form

relies only on

(gauss k)’s normal form, k’s value, and the normal form of +.

k’s value must either be zero or have add1 at the top. We already know that

(gauss 0) has a normal form,

and we just checked that

(gauss (add1 k)) has a normal form for

any Nat k.

A function that assigns a value to every possible argument is called a total function.

Both + and gauss are total.

Are there any functions that aren’t total?

Not here. In Pie, all functions are total.^†

What is an eliminator?

_______________

 ^†Because all functions are total, the order in which subexpressions are evaluated does not matter. If some functions were not total, then the order of evaluation would matter because it would determine whether or not functions were applied to the arguments for which they did not have values.

An eliminator takes apart values built by constructors.

What does it mean to take apart a Nat?

Doesn’t which-Nat take apart a Nat?

This means that which-Nat is an eliminator for Nat. But Nats that have add1 at the top have a smaller Nat tucked under, and which-Nat does not eliminate the smaller Nat.

Is there a way to eliminate the smaller Nat?

One way to eliminate the smaller Nat is with iter-Nat.

What is iter-Nat?

An iter-Nat-expression looks like this:

(iter-Nat target

base

step).

Like which-Nat, when target is zero, the value of the iter-Nat-expression is the value of base.

How is iter-Nat unlike which-Nat?

Unlike which-Nat, when target is (add1 n), the value of the iter-Nat-expression is the value of

(step

(iter-Nat n

base

step)).

So each add1 in the value of target is replaced by a step, and the zero is replaced by base.

That’s right.

What is the normal form of

(iter-Nat 5

3

(λ (smaller)

(add1 smaller)))?

It is 8 because add1 applied five times successively to 3 is 8:

(add1

(add1

(add1

(add1

(add1 3))))).

Is the iter-Nat-expression’s type the same as base’s type?

It must be, because the value of the iter-Nat-expression is the value of base when target is zero.

Let’s use X as a name for base’s type.

What is step’s type?

step is applied to base, and it is also applied to an almost-answer built by step. So step must be an

(→ X

X).

Just as with which-Nat in frame 2:45, the names target, base, and step are convenient ways to refer to iter-Nat’s arguments.

What are the target, base, and step in this iter-Nat-expression?

(iter-Nat 5

3

(λ (k)

(add1 k)))

The target is

5,

The base is

3,

and the step is

(λ (k)

(add1 k)).

Thus far, we have referred to + as if it were completely understood, and assumed that it has a normal form, but there is no definition for +.

What should +’s type be?

+ takes two Nats and returns a Nat.

That’s right.

If recursion were an option, then this would be a proper definition.

How can + be defined with iter-Nat?

Defining + using iter-Nat requires a base and a step. The base is j because of this “same as” chart:

Is there a good way to find the step?

The step is based on the wrapper box in the recursive version of +. It describes how to change an almost-answer, +_n-1, into an answer.

Replace the gray box (which contains the recursion) with the argument to the step as the almost-answer. Remember the white box.

Here goes.

We can’t define a new name unless all the names in both the type and the definition are already defined.^†

_______________

 ^†If definitions could refer to each other, then we could not guarantee that every defined function would be a total function.

And + refers to step-+, which is now defined. This definition deserves a solid box!

Yes, + is now defined.

What is (+ (add1 zero) 7)?

It is 8 because

which is 8.

Can iter-Nat be used to define gauss?

iter-Nat shows a way to repeatedly eliminate the smaller Nat tucked under an add1.

Eliminating the smaller Nat … this sounds like the approach that gauss follows.

Close, but the step doesn’t have enough information. gauss needs an eliminator that combines the expressiveness of both which-Nat and iter-Nat. This eliminator is called rec-Nat.

What is rec-Nat?

The step for rec-Nat is applied to two arguments: the smaller Nat tucked under the add1, and the recursive answer on the smaller Nat. This is the approach used in the definition of gauss in frame 2:59.

This is the rec-Nat pattern.^†

_______________

 ^†The rec-Nat pattern is also referred to as primitive recursion. Thank you, Rózsa Péter (1905–1977), Wilhelm Ackermann (1896–1962), Gabriel Sudan (1899–1977), and David Hilbert (1862–1943).

How can gauss be defined using rec-Nat?

In this frame, there are two definitions of gauss: the dashed box from frame 2:59 and a version using rec-Nat.

What are the differences?

There are three differences:

1. which-Nat is replaced by rec-Nat,
2. the inner λ-expression has one more variable, gauss_n-1, and
3. the recursion (gauss n-1) is replaced by the almost-answer gauss_n-1.

The names n-1 and gauss_n-1 are chosen to be suggestive of what they mean, but they are just variable names.

The arguments to rec-Nat have the same special names as iter-Nat: they are always called target, base, and step.

How can we determine the values of rec-Nat-expressions?

As with iter-Nat, if the target is zero, then the value of the rec-Nat-expression is the value of the base.

What about when the target has add1 at the top?

which-Nat applies its step to the smaller Nat tucked under the add1.

iter-Nat applies its step to an iter-Nat-expression with the same base and step, but with the smaller Nat tucked under add1 as the new target.

How could these be combined?

Here is a guess.

The step is applied to the smaller Nat. The step is, however, also applied to a rec-Nat-expression with the same base and step, but with that very same smaller Nat as the target.

Good guess. When rec-Nat is used with a non-zero Nat as the target, the target shrinks by removing an add1 each time. Once again, the base and step do not change.

What is the value of

(rec-Nat (add1 zero)

0

(λ (n-1 almost)

(add1

(add1 almost))))?

It is the step applied to zero and the new rec-Nat expression. That is,

((λ (n-1 almost)

(add1

(add1 almost)))

zero

(rec-Nat zero

0

(λ (n-1 almost)

(add1

(add1 almost))))).

The resulting expression in the preceding frame is not a value, but it is the same as the original one.

What is the value?

It is

(add1

(add1

(rec-Nat zero

0

(λ (n-1 almost)

(add1

(add1 almost)))))),

which is a value because it has add1 at the top.

What is its normal form?

It is

(add1

(add1 0)).

The target is zero and the base is 0.

A rec-Nat-expression is an expression only if the target is a Nat.

What type should the base and step have?

The base must have some type. Let’s call it X, again. X can be any type, but the rec-Nat-expression has the same type as the base—namely X.

Is that all?

No.

If the base is an X, then the step must be an

(→ Nat X

X).

Why is this the right type for the step?

The step is applied to two arguments: the first is a Nat because it is tucked under an add1 in a target. The second argument is almost. almost is an X because almost is also built by rec-Nat.

How does this relate to the step’s type in which-Nat and iter-Nat?

Like which-Nat, rec-Nat’s step accepts the smaller Nat tucked under the target’s add1. Like iter-Nat, it also accepts the recursive almost-answer.

Here is a function that checks whether a Nat is zero.

_______________

 ^†We use 't and 'nil as two arbitrary values. This may be familiar to Lispers (Thank you, John McCarthy (1927–2011)), but zerop is called zero? in Scheme (Thanks, Gerald J. Sussman (1947–) and Guy L Steele (1954–)).

Why use rec-Nat, which is recursive, to define something that only needs to determine whether the top constructor is zero or add1? After all, which-Nat would have been good enough.

which-Nat is easy to explain, but rec-Nat can do anything that which-Nat (and iter-Nat) can do.

Why are the λ-variables in step-zerop called n-1 and zerop_n-1?

The name n-1 is once again chosen to suggest one less than n because it is one less than the target Nat, that is, the Nat expression being eliminated. The name zerop_n-1 suggests (zerop n-1).

The step is merely a λ-expression, so any other unused variable names would work, but this style of naming variables in steps is used frequently.

Both arguments to step-zerop are unused, which is why they are dim. Thus, the definition only seems to be recursive; in fact, it is not.

What is the point of a λ-expression that does not use its arguments?

The step used with rec-Nat always takes two arguments, though it need not always use them.

What is the value of (zerop 37)?

Let’s see.

The value is determined immediately. The value for 36, which is (add1 35), is not necessary, so there’s no reason to find it.

We need not evaluate expressions until their values actually become necessary. Otherwise, it would take a lot of work to evaluate the argument to step-zerop

(rec-Nat 36

't

step-zerop),

so the “same as” chart would have at least 105 more lines.

Sometimes laziness is a virtue.

Is (zerop 37) the same as (zerop 23)?

Yes indeed.

Here is the step for gauss.

This definition uses the naming convention from frame 44.

Yes, it does.

Another advantage of defining a step is that its type is written explicitly, rather than implied by its use in rec-Nat.

The explicit type does make it easier to read and understand the definition.

λ-variables in a step like zerop_n-1 and gauss_n-1 are almost the answer, in the sense of frame 2:56.

Okay.

What is the solid-box definition of gauss?

Here it is.

What is the base?

What is the step?

It is step-gauss.

Indeed it is.

What is (gauss zero) using this definition?

It is 0 because

(rec-Nat zero

0

step-gauss)

is the same as the second argument to rec-Nat, which is 0.

Here is a start for finding the value of (gauss (add1 zero)).

Now finish finding the value.

Here we go.

which is a value because it has add1 at the top.

Is that value normal?

No, but this chart finds its normal form.

which is indeed normal.

Why is rec-Nat always safe to use?

That’s a good question.

When the target has add1 at its top, then rec-Nat is recursive. If recursion is not an option, why is this acceptable?

If the step does not rely on the almost-answer, as in frame 43, then a value has already been reached. If the step does rely on the almost-answer, then the recursion is guaranteed to reach the base, which is always a value or an expression that becomes a value.

How do we know that?

Because every target Nat is the same as either zero or (add1 n), where n is a smaller Nat.

How do we know that n is smaller?

The only way that it could be the same or larger is if the target Nat were built from infinitely many add1s. But because every function is total, there is no way to do this. Likewise, no step can fail to be total, because here all functions are total, and each step applies a function.

So why can’t we use this style of reasoning for any recursive definition?

This style of reasoning cannot be expressed with our tools. But once we are convinced that rec-Nat with a total step is a way to eliminate any target Nat, we no longer need to reason carefully that each new definition is total.^†

_______________

 ^†Loosely speaking: we can’t, but even if we were able to, it would be exhausting.

Are there more interesting examples of definitions using rec-Nat?

It can be used to define ∗^† to mean multiplication.

In other words, if n and j are Nats, then

(∗ n j)

should be the product of n and j.

_______________

 ^†∗ is pronounced “times.”

∗ takes two Nats and their product is a Nat. So here is ∗’s type.

At each step, + adds one to the answer so far. What does ∗ do at each step?

∗ adds j, its second argument, to the almost-answer.

Here is make-step-∗, which yields a step function for any j.

That doesn’t look like the preceding steps.

No matter what j is, make-step-∗ constructs an appropriate step. This step takes two arguments because steps used with rec-Nat take two arguments, as in step-zerop from frame 46.

Now define ∗

Okay.

The argument to make-step-∗. is j, which is added to the product at each step. The base is 0 because multiplying by zero is 0.

It may look as though make-step-∗ is doing something new. It is a λ-expression that produces a new λ-expression. Instead of this two-step process, it is possible to collapse the nested λs into a single λ.

make-step-∗ produces a step for any given j. And, despite their seeming difference, make-step-∗ and step-∗ have the same definition.

That can’t be the same definition. It has a three-argument λ-expression.

In fact, all λ-expressions expect exactly one argument.

(λ (x y z)

(+ x (+ y z)))

is merely a shorter way of writing

(λ (x)

(λ (y)

(λ (z)

(+ x (+ y z))))).

Does that mean that

(→ Nat Nat Nat

Nat)

is also a shorter way of writing something?

It is a shorter way of writing

(→ Nat

(→ Nat

(→ Nat

Nat))).

If a function takes three arguments, it is possible to apply the function to just one of them.

Is it also possible to apply the function to just two arguments?

If f is an

(→ Nat Nat Nat

Nat)

then

(f x y z)

is merely a shorter way of writing

((f x y) z),

which is a shorter way of writing

(((f x) y) z).

Does this mean that every function takes exactly one argument?

Indeed. Every function takes exactly one argument.

Defining functions that take multiple arguments as nested one-argument functions is called Currying.^†

_______________

 ^†Thank you, Haskell B. Curry (1900–1982) and Moses Ilyich Schönfinkel (1889–1942).

Now the definition of ∗ deserves a box.

Even though step-∗ looks like a three-argument λ-expression, it can be given just one argument. rec-Nat expects that its step is a function that would get exactly two arguments.

Here are the first five lines in the chart for the normal form of (∗ 2 29).

Now, find its normal form.

Ah, Currying is involved.

Are any steps left out of this chart?

Yes, making (+ 29 0) and the resultant (+ 29 29) normal.^†

_______________

 ^†This chart saves paper, energy, and time.

Thanks.

At first, this chart seemed like it would be tedious.

That’s just right.

What is a good name for this definition?

This function always returns 0.

Very observant.

A shortcoming of types like Nat is that they don’t say anything about which Nat was intended. Later, we encounter more powerful types that allow us to talk about particular Nats.^†

_______________

 ^†Actually, the definition in frame 73 was supposed to be factorial. The oversight, however, survived unnoticed in more drafts than the authors would like to admit. We leave the task of correcting it to the reader.

So these powerful types prevent defining five to be 9 as in frame 2:36?

Absolutely not.

Types do not prevent foolishness like defining five to be 9. We can, however, write some of our thoughts as types.

Interesting.

In frame 2:80, we defined Pear as